// -*- mode: Scala;-*- 
// Filename:    generators.scala 
// Authors:     Matt Helige adapted LGM's code
// Creation:    Mon Dec 24 12:01:04 2007 
// Copyright:   Not supplied 

// Description:
//   
//   Approximately a two-level type style decomposition of Milner's
//   factorization of \pi-calculus, but allowing for a reflective
//   interpretation.
//   ------------------------------------------------------------------------

package com.biosimilarity.reflection.paratrope.Eval

import java.net.URL

trait NormalProcesses {
  type Name
  type Agent

  // M,N ::= 0
  //         xA
  //         M+N

  trait NormalProcess
  case object Termination extends NormalProcess
  case class LocatedAgent(x: Name, a: Agent) extends NormalProcess
  case class Sum(summands: List[NormalProcess]) extends NormalProcess

  def locate(x : Name, a : Agent) : NormalProcess = new LocatedAgent(x,a)
}

trait Agents {
  type Name
  type Process

  // A ::= ?(x0,...,xN).P
  //       !(P0,...,PN)

  trait Agent
  case class Abstraction( formals: List[Name], body: Process ) extends Agent
  case class Concretion( actuals: List[Process] ) extends Agent

  def abstrakt( formals : List[Name], body : Process ) : Agent = {
    new Abstraction( formals, body )
  }
  def pack( actuals : List[Process] ) : Agent = {
    new Concretion( actuals )
  }
}

trait Processes {
  type Name
  type NormalProcess

  // P,Q ::= N
  //         P|Q
  //         @x

  trait Process
  case class Tangle( n : NormalProcess ) extends Process
  case class Composition( parands : List[Process] ) extends Process
  case class Transcription( x : Name ) extends Process

  def transcribe( x : Name ) : Process = {
    new Transcription( x )
  }
}

trait Nominals {
  type Process
  type Literal

  // x,y ::= <<P>>

  trait Name
  case class Encoding(code: Process) extends Name
  case class Atom(atom: Literal) extends Name
  def encode(process : Process) : Name = new Encoding( process )
  def process( n : Name ) : Process =
    n match {
      case Encoding( p ) => p
      case Atom( atom ) =>
	throw new Exception( "unbound literal" + atom.toString )
    }
}

trait ConcreteLiterals {
  trait Literal
  case class StringLiteral( s : String ) extends Literal
  case class DeBruijnLiteral( i : Int, j : Int ) extends Literal
  case class URLLiteral( url : java.net.URL ) extends Literal
}

trait Generators
  extends Nominals
  with ConcreteLiterals
  with NormalProcesses
  with Agents
  with Processes {
    val Stop : Process = Tangle( Termination )
    val Mark : Name = encode( Stop )

    def asName( a : Any ) = {
      a match {
	case p : Process => encode( p )
	case s : String => Atom( StringLiteral( s ) )
	case u : java.net.URL => Atom( URLLiteral( u ) )
	case _ => throw new Exception( "no nominal conversion" )
      }
    }

    def nameStream( seed : Any, fresh : Name => Name  ) = {
      lazy val loopStrm : Stream[Name] =
	(List( asName( seed ) ).toStream append (loopStrm map fresh));
      loopStrm
    }
}

object theStandardGenerators extends Generators {
  // These, dear grasshopper, are namespaces -- R E A L namespaces 
  def KleeneNames( seed : String ) = {
    nameStream(
      seed,
      { ( n : Name ) => {
	n match {
	  case Atom( StringLiteral( x ) ) =>
	    Atom( StringLiteral( seed + x ) )
	  case _ =>
	    throw new Exception( "unexpected nominal type" + n.toString )
	}
      } }
    )
  }
  
  def iNames( seed : Process ) = {
    nameStream(
      seed,
      { ( n : Name ) => {
	n match {
	  case Encoding( x ) =>
	    encode(
	      Tangle(
		LocatedAgent( encode( x ), abstrakt( List( Mark ), Stop ) )
	      )
	    )
	  case _ =>
	    throw new Exception( "unexpected nominal type" + n.toString )
	}
      } }
    )
  }

  def oNames( seed : Process ) = {
    nameStream(
      seed,
      { ( n : Name ) => {
	n match {
	  case Encoding( x ) =>
	    encode(
	      Tangle(
		LocatedAgent( encode( x ), pack( List( Stop ) ) )
	      )
	    )
	  case _ =>
	    throw new Exception( "unexpected nominal type" + n.toString )
	}
      } }
    )
  }
}
